T:Type, L:(T List), P:(T).
l_exists(L; T; x.(P(x)))  (reduce((x,y. bor(P(x); y)); ff; L)) 

latex

Definitions	t  T, if b then t else f fi , Y, ff, reduce(f; k; as), b, x:A. B(x), x. t(x), prop{i:l}, P  Q, P  Q, P  Q, x(s), P  Q, guard(T), P  Q, False
Lemmas	bool wf, false wf, l exists wf, assert wf, l exists nil, l exists cons, assert of bor, iff functionality wrt iff, all functionality wrt iff, bfalse wf, reduce wf, bor wf, iff wf